
module MeteoCal

//Modelling
//user
sig User {}

//Date is used to model how much time left from the beginning of the event
//can be more than three days, from 3 to 2 days before and exactly one day before
abstract sig Date{}
one sig MORETHANTHREEDAYSBEFORE extends Date{}
one sig OR2OR3DAYSBEFORE extends Date{}
one sig ONEDAYBEFORE extends Date{}


//revent
sig Event{
	owner : one User,
	participants: set User,
    date : one Date
}


sig OutDoorEvent extends Event{
   weather : one Weather
}

//Weather is used to model the weather forecast for an event
abstract sig Weather{}
one sig BADWEATHER extends Weather{}
one sig GOODWEATHER extends Weather{}


//Notification is used to model a message sent to ta user for somethingS
abstract sig Notification{
	about: one Event,
	sendedTo : some User
}
sig Invitation extends Notification{}
sig WeatherAdvice extends Notification{}
sig Warning extends Notification{}

//if an user create an event he has to participate to that event
fact ifCreateParteciped{
	all e :Event | e.owner in e.participants 
}

//Properties regarding the Invitation
fact invitationProperties{
//an user can' t receive the invitation of its oen event
  (no i : Invitation |i.about.owner in i.sendedTo) &&
//an user can receive an invitation about an event iff it is in the set of participants
  (all i : Invitation | (i.about.participants - i.about.owner) in i.sendedTo)  &&
//un invitation for everry event with more than one participants
  (all e: Event | one i:Invitation |  i.about = e  iff #e.participants > 1 )

}

fact  WarningProperties{
//it does not exist an warning about an event wich has not like date ONEDAYBEFORE
  (no w : Warning| !(w.about.date = ONEDAYBEFORE)  ) &&
//for every event wich have like date ONEDAYBEFORE, there is one warning
  (all e: Event |  one w: Warning | e = w.about iff e.date = ONEDAYBEFORE ) &&
//every participants have to receive the warning about the event
  (all w :  Warning| w.about.participants = w.sendedTo) 
}


fact WeatherAdviceProperties{
//Only the owner can receive this kin of notification
   (all w : WeatherAdvice |  w.sendedTo = w.about.owner) &&
//All weather advice are releated to an event that has bad weather and date from 1 to 3 days before
   (all w : WeatherAdvice | (w.about.date = OR2OR3DAYSBEFORE || w.about.date = ONEDAYBEFORE )     
                 && (w.about.weather = BADWEATHER)) &&
//for every event that has bad weather and date from 1 to 3 days before, exist one weather notification,
//which is releated to this event
  (all e: Event | one w : WeatherAdvice | e = w.about iff 
                                           (e.date = OR2OR3DAYSBEFORE  || w.about.date = ONEDAYBEFORE) &&
                                          ( e.weather = BADWEATHER) )
                           
}

//assertion 
//It is no possible to find an invitation, if there are no participant except the owner 
assert noInvitation{
  no i : Invitation | #i.about.participants = 1
}

//Only the owner can receive the weather advice notification, so the number of th user in sendedTo is one
assert onlyOwner{
  all w : WeatherAdvice |#w.sendedTo =1 
}

//check noInvitation
//check onlyOwner


//Run
pred show(){

}

run show 





	
